(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
minus(0, y) → 0
minus(s(x), 0) → s(x)
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if(true, x, y) → x
if(false, x, y) → y
perfectp(0) → false
perfectp(s(x)) → f(x, s(0), s(x), s(x))
f(0, y, 0, u) → true
f(0, y, s(z), u) → false
f(s(x), 0, z, u) → f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) → if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))
Rewrite Strategy: FULL
(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)
Transformed TRS to relative TRS where S is empty.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
minus(0, y) → 0
minus(s(x), 0) → s(x)
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if(true, x, y) → x
if(false, x, y) → y
perfectp(0) → false
perfectp(s(x)) → f(x, s(0), s(x), s(x))
f(0, y, 0, u) → true
f(0, y, s(z), u) → false
f(s(x), 0, z, u) → f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) → if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))
S is empty.
Rewrite Strategy: FULL
(3) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
f(s(s(x116272_1)), s(y), z, s(0)) →+ if(le(s(x116272_1), y), f(s(s(x116272_1)), minus(y, s(x116272_1)), z, s(0)), if(le(x116272_1, 0), f(x116272_1, s(0), minus(z, s(x116272_1)), s(0)), f(x116272_1, s(0), z, s(0))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2,1].
The pumping substitution is [x116272_1 / s(s(x116272_1))].
The result substitution is [y / 0, z / minus(z, s(x116272_1))].
The rewrite sequence
f(s(s(x116272_1)), s(y), z, s(0)) →+ if(le(s(x116272_1), y), f(s(s(x116272_1)), minus(y, s(x116272_1)), z, s(0)), if(le(x116272_1, 0), f(x116272_1, s(0), minus(z, s(x116272_1)), s(0)), f(x116272_1, s(0), z, s(0))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2,2].
The pumping substitution is [x116272_1 / s(s(x116272_1))].
The result substitution is [y / 0].
(4) BOUNDS(2^n, INF)